\begin{tabbing}
pre{-}init{-}p2(${\it es}$;$i$;${\it ds}$;${\it init}$;$a$;$p$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=pre{-}init{-}p(${\it es}$; $i$; ${\it ds}$; ${\it init}$; $P$)\+
\\[0ex]\& pre{-}p(${\it es}$;$i$;${\it ds}$;$a$;$p$;$P$)
\\[0ex]\& ($\forall$$x$:Id. ($\uparrow$fpf{-}dom(IdDeq; $x$; ${\it ds}$)) $\Rightarrow$ init{-}p(${\it es}$; $i$; ${\it ds}$IdDeq($x$); $x$; ${\it init}$IdDeq($x$)))
\-
\end{tabbing}